package com.googlecode.kipler.satisfiability.completion.rule.formula;

import com.googlecode.kipler.container.dl.FormulaCategory;
import com.googlecode.kipler.container.dl.World;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.completion.rule.CompletionRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.uniformnotation.UntilBetaFormula;
import com.googlecode.kipler.satisfiability.reasoner.Reasoner;
import com.googlecode.kipler.satisfiability.reasoner.ReasonerException;


public class UntilFormulaRule extends CompletionRule {
	private BetaFormulaRule betaRule;

	public UntilFormulaRule(Reasoner reasoner) {
		betaRule = new BetaFormulaRule(reasoner, FormulaCategory.UNTIL,
				new UntilBetaFormula(), true, "Until formula rule");
	}

	public void apply() throws ReasonerException {
		betaRule.apply();
	}

	public WorldConstraintSystem getWcs() {
		return betaRule.getWcs();
	}

	public World getWorld() {
		return betaRule.getWorld();
	}

	public boolean isApplied() {
		return betaRule.isApplied();
	}

	public void setWcs(WorldConstraintSystem wcs) {
		betaRule.setWcs(wcs);
	}

	public void setWorld(World world) {
		betaRule.setWorld(world);
	}

}
